M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id,
ms:((tg:Id  if source(l) = i then M.da(rcv(l,tg)) else Top fi ) List).
M.send(k;l;s;v;ms;i)   

latex

Definitions

x:A. B(x), M.da(a), t  T, , M.send(k;l;s;v;ms;i), z != f(x)  P(a;z), t.1, t.2, P  Q, x  dom(f), x. t(x), if b then t else f fi , tt, ff, Valtype(da;k), MsgA, M.state, M.V(k), a:A fp B(a), x(s), , Unit, P  Q, P & Q,

Lemmas

Id wf, ifthenelse wf, eq id wf, lsrc wf, ma-da wf, rcv wf, top wf, ma-v wf, ma-st wf, IdLnk wf, Knd wf, msga wf, assert wf, deq-member wf, product-deq wf, Kind-deq wf, idlnk-deq wf, fpf-cap wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, concat wf, map wf, pi2 wf, pi1 wf, ma-state wf, fpf-cap-void-subtype, fpf-ap wf, subtype rel self